nLab Schanuel topos

Contents

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Contents

Idea

The Schanuel topos (also called the Myhill-Schanuel topos) is the Grothendieck topos of “combinatorial functors” whose “typical objects are natural combinatorial constructions such as binomial coefficients1. It plays an important role in computer science in the theory of name binding calculi and in William Lawvere‘s approach to petit toposes. It can be viewed as a category-theoretic variant of the Fraenkel-Mostowski model of set theory.

Definition

The Schanuel topos is the sheaf topos Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) where FinSet mono opFinSet^{op}_{mono} is the opposite of the category of finite sets and monomorphisms and the coverage is the collection of all sieves generated by singletons {f}.\{f\}\quad.

Properties

  • The objects of the Schanuel topos are called nominal sets and correspond precisely to the pullback preserving functors FinSet monoSetFinSet_{mono}\to Set.

  • Since monos are precisely the morphisms that pull back along themselves to isomorphisms, any pullback preserving functor preserves monos. This affords another description as the category of intersection preserving functors from FinSet monoSet monoFinSet_{mono}\to Set_{mono}, a special case of combinatorial functors.

  • The Schanuel topos Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is atomic over SetSet (S. Schanuel, cf. (Wraith 1978), p.335) hence Boolean. This fact can be viewed as a reflex of the urelements in Fraenkel-Mostowski set theory.

  • The Schanuel topos Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is locally finitely presentable since its category of atoms is co-well-founded? (cf. Marquès 2024).

  • Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is the classifying topos Set[D ]Set[D_\infty] for the theory of infinite decidable objects D D_\infty i.e. for a Grothendieck topos \mathcal{E} geometric morphisms Sh(FinSet mono op,J)\mathcal{E}\to Sh(FinSet^{op}_{mono},J) correspond to infinite decidable objects in \mathcal{E}. Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is equivalent to Sh ¬¬([FinSet mono,Set])Sh_{\neg\neg}([FinSet_mono,Set]) where [FinSet mono,Set][FinSet_mono,Set] classifies decidable objects.

  • Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is the category of continuous actions for the group of bijections of NN equipped with the topology derived from the product topology for NN.\prod_{N}N\quad .

  • Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is the Kleisli category of the monad on the topos of species Set FinSet isoSet^{FinSet_{iso}} induced by the inclusion of finite sets and bijections FinSet isoFinSet monoFinSet_{iso}\hookrightarrow FinSet_{mono} (cf. Fiore-Menni 2004).

  • Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is contractible in the sense of natural homotopy (cf. Joyal-Wraith 1984).

Remark

For some information on the history of the Schanuel topos see section 10 of Menni (2009, pp.529f).

References

  • M. Fiore, M. Menni, Reflective Kleisli Subcategories of the Category of Eilenberg-Moore Algebras for Factorization Monads , TAC 15 no. 2 (2004) pp.40-65. (pdf)

  • M. J. Gabbay, A. M. Pitts, A new approach to abstract syntax with variable binding, Formal Aspects of Computing 13 (2002) pp.341-363. (draft)

  • Peter Johnstone, Sketches of an Elephant vols. I,II, Oxford UP 2002. (pp.79f, 691, 925)

  • André Joyal, Gavin Wraith, Eilenberg-Mac Lane Toposes and Cohomology , pp.117-131 in Cont. Math. 92 AMS 1984.

  • F. William Lawvere, Qualitative Distinctions between some Toposes of Generalized Graphs, Cont. Math. 92 (1989) (p. 298 ff).

  • S. Mac Lane, I. Moerdijk, Sheaves in Geometry and Logic, Springer Heidelberg 1994. (pp.155, 158)

  • Jérémie Marquès?, Atomic Toposes with Co-Well-Founded Categories of Atoms , arXiv:2406.14346 (2024). (abstract)

  • Matías Menni, About N-quantifiers , Appl. Cat. Struc. 11 (2003) pp.421-445. (preprint)

  • Matías Menni, Algebraic categories whose projectives are explicitly free , TAC 22 no.20 (2009) pp.509-541. (abstract)

  • John Myhill, Recursive equivalence types and combinatorial functions , Bull. Amer. Math. Soc. 64 (1958) pp.373-376.

  • Andrew M. Pitts, Nominal Sets - Names and Symmetry in Computer Science , Cambridge UP 2013. (Section 6.3)

  • Alex Simpson, Equivalence and Conditional Independence in Atomic Sheaf Logic, arXiv:2405.11073 (2024). (abstract)

  • Sam Staton, Name-passing process calculi: operational models and structural operational semantics, Technical Report 688 CL University Cambridge 2007. (pdf)

  • G. Wraith, Intuitionistic Algebra: Some Recent Developments of Topos Theory , Proc. ICM Helsinki (1978) pp.331-337. (pdf)


  1. Lawvere 1989, p.299.

Last revised on September 27, 2024 at 17:03:45. See the history of this page for a list of all contributions to it.